Step of Proof: nth_tl_append 11,40
Inference at * 1 
Iof proof for Lemma nth tl append:



1. T : Type
2. T List
  bs:(T List). bs ~ bs 
latex
 by Auto 
latex

 .

DefinitionsType, x:A. B(x), x:AB(x), type List, s ~ t

origin